ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), k:Knd, x:Id, n:,
f:(decl-state(ds)ma-valtype(da; k)fpf-cap(ds; id-deq; x; void)).
update-spec1(k; x; n; s,v.f(s,v))  update-spec(ds; da) 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, , void, id-deq, x.A(x), fpf-cap(f; eq; x; z), top, Kind-deq, x:AB(x), decl-state(ds), <a, b>, t.2, t.1, x:A  B(x), type List, [], f(a), x(s1,s2), cons(car; cdr), fpf-single(x; v), ma-valtype(da; k), update-spec1(k; x; n; s,v.f(s;v)), update-spec(ds; da)
Lemmas	fpf-single wf, pi1 wf, pi2 wf, decl-state wf, Kind-deq wf, top wf, fpf-cap wf, id-deq wf, nat wf, Knd wf, fpf wf, Id wf